SherbyNet - /page/wikibook/entry.mu

Micron Document

<!DOCTYPE html>

<title>Static program analysis</title>

</head>

<span id="openzim-page-title" class="mw-page-title-main"><span class="mw-page-title-main">Static program analysis</span></span>

</h1>

</header>

/* start https://en.wikipedia.org/ */

.mw-parser-output .hlist dl,.mw-parser-output .hlist ol,.mw-parser-output .hlist ul{margin:0;padding:0}.mw-parser-output .hlist dd,.mw-parser-output .hlist dt,.mw-parser-output .hlist li{margin:0;display:inline}.mw-parser-output .hlist.inline,.mw-parser-output .hlist.inline dl,.mw-parser-output .hlist.inline ol,.mw-parser-output .hlist.inline ul,.mw-parser-output .hlist dl dl,.mw-parser-output .hlist dl ol,.mw-parser-output .hlist dl ul,.mw-parser-output .hlist ol dl,.mw-parser-output .hlist ol ol,.mw-parser-output .hlist ol ul,.mw-parser-output .hlist ul dl,.mw-parser-output .hlist ul ol,.mw-parser-output .hlist ul ul{display:inline}.mw-parser-output .hlist .mw-empty-li{display:none}.mw-parser-output .hlist dt::after{content:": "}.mw-parser-output .hlist dd::after,.mw-parser-output .hlist li::after{content:" · ";font-weight:bold}.mw-parser-output .hlist dd:last-child::after,.mw-parser-output .hlist dt:last-child::after,.mw-parser-output .hlist li:last-child::after{content:none}.mw-parser-output .hlist dd dd:first-child::before,.mw-parser-output .hlist dd dt:first-child::before,.mw-parser-output .hlist dd li:first-child::before,.mw-parser-output .hlist dt dd:first-child::before,.mw-parser-output .hlist dt dt:first-child::before,.mw-parser-output .hlist dt li:first-child::before,.mw-parser-output .hlist li dd:first-child::before,.mw-parser-output .hlist li dt:first-child::before,.mw-parser-output .hlist li li:first-child::before{content:" (";font-weight:normal}.mw-parser-output .hlist dd dd:last-child::after,.mw-parser-output .hlist dd dt:last-child::after,.mw-parser-output .hlist dd li:last-child::after,.mw-parser-output .hlist dt dd:last-child::after,.mw-parser-output .hlist dt dt:last-child::after,.mw-parser-output .hlist dt li:last-child::after,.mw-parser-output .hlist li dd:last-child::after,.mw-parser-output .hlist li dt:last-child::after,.mw-parser-output .hlist li li:last-child::after{content:")";font-weight:normal}.mw-parser-output .hlist ol{counter-reset:listitem}.mw-parser-output .hlist ol>li{counter-increment:listitem}.mw-parser-output .hlist ol>li::before{content:" "counter(listitem)"\a0 "}.mw-parser-output .hlist dd ol>li:first-child::before,.mw-parser-output .hlist dt ol>li:first-child::before,.mw-parser-output .hlist li ol>li:first-child::before{content:" ("counter(listitem)"\a0 "}

/* end https://en.wikipedia.org/ */

</style><style data-mw-deduplicate="TemplateStyles:r1246091330">

/* start https://en.wikipedia.org/ */

.mw-parser-output .sidebar{width:22em;float:right;clear:right;margin:0.5em 0 1em 1em;background:var(--background-color-neutral-subtle,#f8f9fa);border:1px solid var(--border-color-base,#a2a9b1);padding:0.2em;text-align:center;line-height:1.4em;font-size:88%;border-collapse:collapse;display:table}body.skin-minerva .mw-parser-output .sidebar{display:table!important;float:right!important;margin:0.5em 0 1em 1em!important}.mw-parser-output .sidebar-subgroup{width:100%;margin:0;border-spacing:0}.mw-parser-output .sidebar-left{float:left;clear:left;margin:0.5em 1em 1em 0}.mw-parser-output .sidebar-none{float:none;clear:both;margin:0.5em 1em 1em 0}.mw-parser-output .sidebar-outer-title{padding:0 0.4em 0.2em;font-size:125%;line-height:1.2em;font-weight:bold}.mw-parser-output .sidebar-top-image{padding:0.4em}.mw-parser-output .sidebar-top-caption,.mw-parser-output .sidebar-pretitle-with-top-image,.mw-parser-output .sidebar-caption{padding:0.2em 0.4em 0;line-height:1.2em}.mw-parser-output .sidebar-pretitle{padding:0.4em 0.4em 0;line-height:1.2em}.mw-parser-output .sidebar-title,.mw-parser-output .sidebar-title-with-pretitle{padding:0.2em 0.8em;font-size:145%;line-height:1.2em}.mw-parser-output .sidebar-title-with-pretitle{padding:0.1em 0.4em}.mw-parser-output .sidebar-image{padding:0.2em 0.4em 0.4em}.mw-parser-output .sidebar-heading{padding:0.1em 0.4em}.mw-parser-output .sidebar-content{padding:0 0.5em 0.4em}.mw-parser-output .sidebar-content-with-subgroup{padding:0.1em 0.4em 0.2em}.mw-parser-output .sidebar-above,.mw-parser-output .sidebar-below{padding:0.3em 0.8em;font-weight:bold}.mw-parser-output .sidebar-collapse .sidebar-above,.mw-parser-output .sidebar-collapse .sidebar-below{border-top:1px solid #aaa;border-bottom:1px solid #aaa}.mw-parser-output .sidebar-navbar{text-align:right;font-size:115%;padding:0 0.4em 0.4em}.mw-parser-output .sidebar-list-title{padding:0 0.4em;text-align:left;font-weight:bold;line-height:1.6em;font-size:105%}.mw-parser-output .sidebar-list-title-c{padding:0 0.4em;text-align:center;margin:0 3.3em}@media(max-width:640px){body.mediawiki .mw-parser-output .sidebar{width:100%!important;clear:both;float:none!important;margin-left:0!important;margin-right:0!important}}body.skin--responsive .mw-parser-output .sidebar a>img{max-width:none!important}@media screen{html.skin-theme-clientpref-night .mw-parser-output .sidebar:not(.notheme) .sidebar-list-title,html.skin-theme-clientpref-night .mw-parser-output .sidebar:not(.notheme) .sidebar-title-with-pretitle{background:transparent!important}html.skin-theme-clientpref-night .mw-parser-output .sidebar:not(.notheme) .sidebar-title-with-pretitle a{color:var(--color-progressive)!important}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .sidebar:not(.notheme) .sidebar-list-title,html.skin-theme-clientpref-os .mw-parser-output .sidebar:not(.notheme) .sidebar-title-with-pretitle{background:transparent!important}html.skin-theme-clientpref-os .mw-parser-output .sidebar:not(.notheme) .sidebar-title-with-pretitle a{color:var(--color-progressive)!important}}@media print{body.ns-0 .mw-parser-output .sidebar{display:none!important}}

/* end https://en.wikipedia.org/ */

</style><table class="sidebar sidebar-collapse nomobile"><tbody><tr><td class="sidebar-pretitle">Part of a series on</td></tr><tr><th class="sidebar-title-with-pretitle"><a href="Software_development" title="Software development">Software development</a></th></tr><tr><td class="sidebar-content">

<div class="sidebar-list mw-collapsible mw-collapsed"><div class="sidebar-list-title" style="color: var(--color-base)">Core activities</div><div class="sidebar-list-content mw-collapsible-content hlist">

<ul><li><a href="Data_modeling" title="Data modeling">Data modeling</a></li>

<li><a href="Software_development_process" title="Software development process">Processes</a></li>

<li><a href="Requirements_analysis" title="Requirements analysis">Requirements</a></li>

<li><a href="Software_design" title="Software design">Design</a></li>

<li><a href="Software_construction" title="Software construction">Construction</a></li>

<li><a href="Software_engineering" title="Software engineering">Engineering</a></li>

<li><a href="Software_testing" title="Software testing">Testing</a></li>

<li><a href="Debugging" title="Debugging">Debugging</a></li>

<li><a href="Software_deployment" title="Software deployment">Deployment</a></li>

<li><a href="Software_maintenance" title="Software maintenance">Maintenance</a></li></ul></div></div></td>

</tr><tr><td class="sidebar-content">

<div class="sidebar-list mw-collapsible mw-collapsed"><div class="sidebar-list-title" style="color: var(--color-base)">Paradigms and models</div><div class="sidebar-list-content mw-collapsible-content hlist">

<ul><li><a href="Agile_software_development" title="Agile software development">Agile</a></li>

<li><a href="Cleanroom_software_engineering" title="Cleanroom software engineering">Cleanroom</a></li>

<li><a href="Incremental_build_model" title="Incremental build model">Incremental</a></li>

<li><a href="Software_prototyping" title="Software prototyping">Prototyping</a></li>

<li><a href="Spiral_model" title="Spiral model">Spiral</a></li>

<li><a href="V-model_(software_development)" title="V-model (software development)">V model</a></li>

<li><a href="Waterfall_model" title="Waterfall model">Waterfall</a></li></ul></div></div></td>

</tr><tr><td class="sidebar-content">

<div class="sidebar-list mw-collapsible mw-collapsed"><div class="sidebar-list-title" style="color: var(--color-base)"><a href="Software_development_methodology" class="mw-redirect" title="Software development methodology">Methodologies</a> and frameworks</div><div class="sidebar-list-content mw-collapsible-content hlist">

<li><a href="DevOps" title="DevOps">DevOps</a></li>

<li><a href="Kanban_(development)" title="Kanban (development)">Kanban</a></li>

<li><a href="Scrum_(software_development)" title="Scrum (software development)">Scrum</a></li>

<li><a href="SEMAT" title="SEMAT">SEMAT</a></li>

</tr><tr><td class="sidebar-content">

<div class="sidebar-list mw-collapsible mw-collapsed"><div class="sidebar-list-title" style="color: var(--color-base)">Supporting disciplines</div><div class="sidebar-list-content mw-collapsible-content hlist">

<ul><li><a href="Software_configuration_management" title="Software configuration management">Configuration management</a></li>

<li><a href="Deployment_management#Computer_science" title="Deployment management">Deployment management</a></li>

<li><a href="Software_documentation" title="Software documentation">Documentation</a></li>

<li><a href="Software_project_management" title="Software project management">Project management</a></li>

<li><a href="Software_quality_assurance" title="Software quality assurance">Quality assurance</a></li>

<li><a href="User_experience" title="User experience">User experience</a></li></ul></div></div></td>

</tr><tr><td class="sidebar-content">

<div class="sidebar-list mw-collapsible mw-collapsed"><div class="sidebar-list-title" style="color: var(--color-base)">Practices</div><div class="sidebar-list-content mw-collapsible-content hlist">

<li><a href="Stand-up_meeting" title="Stand-up meeting">Stand-up</a></li>

</tr><tr><td class="sidebar-content">

<div class="sidebar-list mw-collapsible mw-collapsed"><div class="sidebar-list-title" style="color: var(--color-base)"><a href="Programming_tool" title="Programming tool">Tools</a></div><div class="sidebar-list-content mw-collapsible-content hlist">

<ul><li><a href="Build_automation" title="Build automation">Build automation</a></li>

<li><a href="Compiler" title="Compiler">Compiler</a></li>

<li><a href="Debugger" title="Debugger">Debugger</a></li>

<li><a href="Graphical_user_interface_builder" title="Graphical user interface builder">GUI builder</a></li>

<li><a href="Infrastructure_as_code" title="Infrastructure as code">Infrastructure as code</a></li>

<li><a href="Profiling_(computer_programming)" title="Profiling (computer programming)">Profiler</a></li>

<li><a href="Application-release_automation" title="Application-release automation">Release automation</a></li>

<li><a href="UML_tool" title="UML tool">UML Modeling</a></li></ul></div></div></td>

</tr><tr><td class="sidebar-content">

<div class="sidebar-list mw-collapsible mw-collapsed"><div class="sidebar-list-title" style="color: var(--color-base)">Standards and bodies of knowledge</div><div class="sidebar-list-content mw-collapsible-content hlist">

<li><a href="IEEE_Standards_Association" title="IEEE Standards Association">IEEE standards</a></li>

<li><a href="ISO/IEC_JTC_1/SC_7" title="ISO/IEC JTC 1/SC 7">ISO/IEC standards</a></li>

<li><a href="Project_Management_Body_of_Knowledge" title="Project Management Body of Knowledge">PMBOK</a></li>

<li><a href="Software_Engineering_Body_of_Knowledge" title="Software Engineering Body of Knowledge">SWEBOK</a></li></ul></div></div></td>

</tr><tr><td class="sidebar-content">

<div class="sidebar-list mw-collapsible mw-collapsed"><div class="sidebar-list-title" style="color: var(--color-base)">Glossaries</div><div class="sidebar-list-content mw-collapsible-content hlist">

<ul><li><a href="Glossary_of_artificial_intelligence" title="Glossary of artificial intelligence">Artificial intelligence</a></li>

<li><a href="Glossary_of_computer_science" title="Glossary of computer science">Computer science</a></li>

<li><a href="Glossary_of_electrical_and_electronics_engineering" title="Glossary of electrical and electronics engineering">Electrical and electronics engineering</a></li></ul></div></div></td>

</tr><tr><td class="sidebar-content">

<div class="sidebar-list mw-collapsible mw-collapsed"><div class="sidebar-list-title" style="color: var(--color-base)">Outlines</div><div class="sidebar-list-content mw-collapsible-content hlist">

<ul><li><a href="Outline_of_software_development" title="Outline of software development">Outline of software development</a></li></ul></div></div></td>

</tr><tr><td class="sidebar-navbar"><style data-mw-deduplicate="TemplateStyles:r1239400231">

/* start https://en.wikipedia.org/ */

.mw-parser-output .navbar{display:inline;font-size:88%;font-weight:normal}.mw-parser-output .navbar-collapse{float:left;text-align:left}.mw-parser-output .navbar-boxtext{word-spacing:0}.mw-parser-output .navbar ul{display:inline-block;white-space:nowrap;line-height:inherit}.mw-parser-output .navbar-brackets::before{margin-right:-0.125em;content:"[ "}.mw-parser-output .navbar-brackets::after{margin-left:-0.125em;content:" ]"}.mw-parser-output .navbar li{word-spacing:-0.125em}.mw-parser-output .navbar a>span,.mw-parser-output .navbar a>abbr{text-decoration:inherit}.mw-parser-output .navbar-mini abbr{font-variant:small-caps;border-bottom:none;text-decoration:none;cursor:inherit}.mw-parser-output .navbar-ct-full{font-size:114%;margin:0 7em}.mw-parser-output .navbar-ct-mini{font-size:114%;margin:0 4em}html.skin-theme-clientpref-night .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}@media(prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}}@media print{.mw-parser-output .navbar{display:none!important}}

/* end https://en.wikipedia.org/ */

</style></td></tr></tbody></table>

<p>In <a href="Computer_science" title="Computer science">computer science</a>, <b>static program analysis</b> (also known as <b>static analysis</b> or <b>static simulation</b>) is the <a href="Program_analysis" title="Program analysis">analysis</a> of computer programs performed without executing them, in contrast with <a href="Dynamic_program_analysis" title="Dynamic program analysis">dynamic program analysis</a>, which is performed on programs during their execution in the integrated environment.<sup id="cite_ref-1" class="reference"><a href="#cite_note-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup><sup id="cite_ref-2" class="reference"><a href="#cite_note-2"><span class="cite-bracket">[</span>2<span class="cite-bracket">]</span></a></sup>

</p><p>The term is usually applied to analysis performed by an automated tool, with human analysis typically being called "program understanding", <a href="Program_comprehension" title="Program comprehension">program comprehension</a>, or <a href="Code_review" title="Code review">code review</a>. In the last of these, <a href="Software_inspection" title="Software inspection">software inspection</a> and <a href="Software_walkthrough" title="Software walkthrough">software walkthroughs</a> are also used. In most cases the analysis is performed on some version of a program's <a href="Source_code" title="Source code">source code</a>, and, in other cases, on some form of its <a href="Object_code" title="Object code">object code</a>.

</p>

<div class="mw-heading mw-heading2"><h2 id="Rationale">Rationale</h2></div>

<p>The sophistication of the analysis performed by tools varies from those that only consider the behaviour of individual statements and declarations,<sup id="cite_ref-3" class="reference"><a href="#cite_note-3"><span class="cite-bracket">[</span>3<span class="cite-bracket">]</span></a></sup> to those that include the complete <a href="Source_code" title="Source code">source code</a> of a program in their analysis. The uses of the information obtained from the analysis vary from highlighting possible coding errors (e.g., the <a href="Lint_programming_tool" class="mw-redirect" title="Lint programming tool">lint</a> tool) to <a href="Formal_methods" title="Formal methods">formal methods</a> that mathematically prove properties about a given program (e.g., its behaviour matches that of its specification).

</p><p><a href="Software_metric" title="Software metric">Software metrics</a> and <a href="Reverse_engineering" title="Reverse engineering">reverse engineering</a> can be described as forms of static analysis. Deriving software metrics and static analysis are increasingly deployed together, especially in creation of embedded systems, by defining so-called <i>software quality objectives</i>.<sup id="cite_ref-4" class="reference"><a href="#cite_note-4"><span class="cite-bracket">[</span>4<span class="cite-bracket">]</span></a></sup>

</p><p>A growing commercial use of static analysis is in the verification of properties of software used in <a href="Safety-critical" class="mw-redirect" title="Safety-critical">safety-critical</a> computer systems and

locating potentially <a href="Vulnerability_(computing)" class="mw-redirect" title="Vulnerability (computing)">vulnerable</a> code.<sup id="cite_ref-5" class="reference"><a href="#cite_note-5"><span class="cite-bracket">[</span>5<span class="cite-bracket">]</span></a></sup> For example, the following industries have identified the use of static code analysis as a means of improving the quality of increasingly sophisticated and complex software:

</p>

<ol><li><a href="Medical_software" title="Medical software">Medical software</a>: The US <a href="Food_and_Drug_Administration" title="Food and Drug Administration">Food and Drug Administration</a> (FDA) has identified the use of static analysis for medical devices.<sup id="cite_ref-6" class="reference"><a href="#cite_note-6"><span class="cite-bracket">[</span>6<span class="cite-bracket">]</span></a></sup></li>

<li>Nuclear software: In the UK the Office for Nuclear Regulation (ONR) recommends the use of static analysis on <a href="Reactor_protection_system" title="Reactor protection system">reactor protection systems</a>.<sup id="cite_ref-7" class="reference"><a href="#cite_note-7"><span class="cite-bracket">[</span>7<span class="cite-bracket">]</span></a></sup></li>

<li>Aviation software (in combination with <a href="Dynamic_program_analysis" title="Dynamic program analysis">dynamic analysis</a>).<sup id="cite_ref-8" class="reference"><a href="#cite_note-8"><span class="cite-bracket">[</span>8<span class="cite-bracket">]</span></a></sup></li>

<li>Automotive & Machines (functional safety features form an integral part of each automotive product development phase, <a href="ISO_26262" title="ISO 26262">ISO 26262</a>, section 8).</li></ol>

<p>A study in 2012 by VDC Research reported that 28.7% of the embedded software engineers surveyed use static analysis tools and 39.7% expect to use them within 2 years.<sup id="cite_ref-9" class="reference"><a href="#cite_note-9"><span class="cite-bracket">[</span>9<span class="cite-bracket">]</span></a></sup>

A study from 2010 found that 60% of the interviewed developers in European research projects made at least use of their basic IDE built-in static analyzers. However, only about 10% employed an additional other (and perhaps more advanced) analysis tool.<sup id="cite_ref-10" class="reference"><a href="#cite_note-10"><span class="cite-bracket">[</span>10<span class="cite-bracket">]</span></a></sup>

</p><p>In the application security industry the name <a href="Static_application_security_testing" title="Static application security testing">static application security testing</a> (SAST) is also used. SAST is an important part of <a href="Security_Development_Lifecycle" class="mw-redirect" title="Security Development Lifecycle">Security Development Lifecycles</a> (SDLs) such as the SDL defined by Microsoft<sup id="cite_ref-11" class="reference"><a href="#cite_note-11"><span class="cite-bracket">[</span>11<span class="cite-bracket">]</span></a></sup> and a common practice in software companies.<sup id="cite_ref-12" class="reference"><a href="#cite_note-12"><span class="cite-bracket">[</span>12<span class="cite-bracket">]</span></a></sup>

</p>

<div class="mw-heading mw-heading2"><h2 id="Tool_types">Tool types</h2></div>

<p>The OMG (<a href="Object_Management_Group" title="Object Management Group">Object Management Group</a>) published a study regarding the types of software analysis required for <a href="Software_quality" title="Software quality">software quality</a> measurement and assessment. This document on "How to Deliver Resilient, Secure, Efficient, and Easily Changed IT Systems in Line with CISQ Recommendations" describes three levels of software analysis.<sup id="cite_ref-13" class="reference"><a href="#cite_note-13"><span class="cite-bracket">[</span>13<span class="cite-bracket">]</span></a></sup>

</p>

<dl><dt>Unit Level</dt>

<dd>Analysis that takes place within a specific program or subroutine, without connecting to the context of that program.</dd>

<dt>Technology Level</dt>

<dd>Analysis that takes into account interactions between unit programs to get a more holistic and semantic view of the overall program in order to find issues and avoid obvious false positives.</dd>

<dt>System Level</dt>

<dd>Analysis that takes into account the interactions between unit programs, but without being limited to one specific technology or programming language.</dd></dl>

<p>A further level of software analysis can be defined.

</p>

<dl><dt>Mission/Business Level</dt>

<dd>Analysis that takes into account the business/mission layer terms, rules and processes that are implemented within the software system for its operation as part of enterprise or program/mission layer activities. These elements are implemented without being limited to one specific technology or programming language and in many cases are distributed across multiple languages, but are statically extracted and analyzed for system understanding for mission assurance.</dd></dl>

<div class="mw-heading mw-heading2"><h2 id="Formal_methods">Formal methods</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .hatnote{font-style:italic}.mw-parser-output div.hatnote{padding-left:1.6em;margin-bottom:0.5em}.mw-parser-output .hatnote i{font-style:normal}.mw-parser-output .hatnote+link+.hatnote{margin-top:-0.5em}@media print{body.ns-0 .mw-parser-output .hatnote{display:none!important}}

/* end https://en.wikipedia.org/ */

</style><div role="note" class="hatnote navigation-not-searchable">Main article: <a href="Formal_methods" title="Formal methods">Formal methods</a></div>

<p>Formal methods is the term applied to the analysis of <a href="Software" title="Software">software</a> (and <a href="Computer_hardware" title="Computer hardware">computer hardware</a>) whose results are obtained purely through the use of rigorous mathematical methods. The mathematical techniques used include <a href="Denotational_semantics" title="Denotational semantics">denotational semantics</a>, <a href="Axiomatic_semantics" title="Axiomatic semantics">axiomatic semantics</a>, <a href="Operational_semantics" title="Operational semantics">operational semantics</a>, and <a href="Abstract_interpretation" title="Abstract interpretation">abstract interpretation</a>.

</p><p>By a straightforward reduction to the <a href="Halting_problem" title="Halting problem">halting problem</a>, it is possible to prove that (for any <a href="Turing_complete" class="mw-redirect" title="Turing complete">Turing complete</a> language), finding all possible run-time errors in an arbitrary program (or more generally any kind of violation of a specification on the final result of a program) is <a href="Decision_problem" title="Decision problem">undecidable</a>: there is no mechanical method that can always answer truthfully whether an arbitrary program may or may not exhibit runtime errors. This result dates from the works of <a href="Alonzo_Church" title="Alonzo Church">Church</a>, <a href="Kurt_G%C3%B6del" title="Kurt Gödel">Gödel</a> and <a href="Alan_Turing" title="Alan Turing">Turing</a> in the 1930s (see: <a href="Halting_problem" title="Halting problem">Halting problem</a> and <a href="Rice's_theorem" title="Rice's theorem">Rice's theorem</a>). As with many undecidable questions, one can still attempt to give useful approximate solutions.

</p><p>Some of the implementation techniques of formal static analysis include:<sup id="cite_ref-14" class="reference"><a href="#cite_note-14"><span class="cite-bracket">[</span>14<span class="cite-bracket">]</span></a></sup>

</p>

<ul><li><a href="Abstract_interpretation" title="Abstract interpretation">Abstract interpretation</a>, to model the effect that every statement has on the state of an abstract machine (i.e., it 'executes' the software based on the mathematical properties of each statement and declaration). This abstract machine over-approximates the behaviours of the system: the abstract system is thus made simpler to analyze, at the expense of <i>incompleteness</i> (not every property true of the original system is true of the abstract system). If properly done, though, abstract interpretation is <i>sound</i> (every property true of the abstract system can be mapped to a true property of the original system).<sup id="cite_ref-15" class="reference"><a href="#cite_note-15"><span class="cite-bracket">[</span>15<span class="cite-bracket">]</span></a></sup></li>

<li><a href="Data_flow_analysis" class="mw-redirect" title="Data flow analysis">Data-flow analysis</a>, a lattice-based technique for gathering information about the possible set of values;</li>

<li><a href="Hoare_logic" title="Hoare logic">Hoare logic</a>, a <a href="Formal_system" title="Formal system">formal system</a> with a set of logical rules for reasoning rigorously about the <a href="Correctness_of_computer_programs" class="mw-redirect" title="Correctness of computer programs">correctness of computer programs</a>. There is tool support for some programming languages (e.g., the <a href="SPARK_programming_language" class="mw-redirect" title="SPARK programming language">SPARK programming language</a> (a subset of <a href="Ada_(programming_language)" title="Ada (programming language)">Ada</a>) and the <a href="Java_Modeling_Language" title="Java Modeling Language">Java Modeling Language</a>—JML—using <a href="ESC/Java" title="ESC/Java">ESC/Java</a> and <a href="ESC/Java2" class="mw-redirect" title="ESC/Java2">ESC/Java2</a>, Frama-C WP (<a href="Weakest_precondition" class="mw-redirect" title="Weakest precondition">weakest precondition</a>) plugin for the C language extended with ACSL (<a href="ANSI/ISO_C_Specification_Language" title="ANSI/ISO C Specification Language">ANSI/ISO C Specification Language</a>) ).</li>

<li><a href="Model_checking" title="Model checking">Model checking</a>, considers systems that have <a href="Finite-state_machine" title="Finite-state machine">finite state</a> or may be reduced to finite state by <a href="Abstraction_(computer_science)" title="Abstraction (computer science)">abstraction</a>;</li>

<li><a href="Symbolic_execution" title="Symbolic execution">Symbolic execution</a>, as used to derive mathematical expressions representing the value of mutated variables at particular points in the code.</li>

<li><a href="Nullable" class="mw-redirect" title="Nullable">Nullable</a> reference analysis</li></ul>

<div class="mw-heading mw-heading2"><h2 id="Data-driven_static_analysis">Data-driven static analysis</h2></div>

<p>Data-driven static analysis leverages extensive codebases to infer coding rules and improve the accuracy of the analysis.<sup id="cite_ref-dewes_16-0" class="reference"><a href="#cite_note-dewes-16"><span class="cite-bracket">[</span>16<span class="cite-bracket">]</span></a></sup><sup id="cite_ref-17" class="reference"><a href="#cite_note-17"><span class="cite-bracket">[</span>17<span class="cite-bracket">]</span></a></sup> For instance, one can use all Java open-source packages available on <a href="GitHub" title="GitHub">GitHub</a> to learn good analysis strategies. The rule inference can use machine learning techniques.<sup id="cite_ref-OhYang2015_18-0" class="reference"><a href="#cite_note-OhYang2015-18"><span class="cite-bracket">[</span>18<span class="cite-bracket">]</span></a></sup> It is also possible to learn from a large amount of past fixes and warnings.<sup id="cite_ref-dewes_16-1" class="reference"><a href="#cite_note-dewes-16"><span class="cite-bracket">[</span>16<span class="cite-bracket">]</span></a></sup>

</p>

<div class="mw-heading mw-heading2"><h2 id="Remediation">Remediation</h2></div>

<p>Static analyzers produce warnings. For certain types of warnings, it is possible to design and implement <a href="Automatic_bug_fixing" title="Automatic bug fixing">automated remediation</a> techniques. For example, Logozzo and Ball have proposed automated remediations for C# <i>cccheck</i>.<sup id="cite_ref-19" class="reference"><a href="#cite_note-19"><span class="cite-bracket">[</span>19<span class="cite-bracket">]</span></a></sup>

</p>

/* start https://en.wikipedia.org/ */

.mw-parser-output .div-col{margin-top:0.3em;column-width:30em}.mw-parser-output .div-col-small{font-size:90%}.mw-parser-output .div-col-rules{column-rule:1px solid #aaa}.mw-parser-output .div-col dl,.mw-parser-output .div-col ol,.mw-parser-output .div-col ul{margin-top:0}.mw-parser-output .div-col li,.mw-parser-output .div-col dd{page-break-inside:avoid;break-inside:avoid-column}

/* end https://en.wikipedia.org/ */

</style><div class="div-col" style="column-width: 30em;">

<ul><li><a href="Code_audit" title="Code audit">Code audit</a></li>

<li><a href="Documentation_generator" title="Documentation generator">Documentation generator</a></li>

<li><a href="Formal_semantics_of_programming_languages" class="mw-redirect" title="Formal semantics of programming languages">Formal semantics of programming languages</a></li>

<li><a href="Formal_verification" title="Formal verification">Formal verification</a></li>

<li><a href="ISO/IEC_9126" title="ISO/IEC 9126">ISO 9126</a> (now ISO 25000 series)</li>

<li><a href="Lint_(software)" title="Lint (software)">Lint (software)</a></li>

<li><a href="List_of_tools_for_static_code_analysis" title="List of tools for static code analysis">List of tools for static code analysis</a></li>

<li><a href="Shape_analysis_(program_analysis)" title="Shape analysis (program analysis)">Shape analysis</a></li>

<li><a href="Software_quality" title="Software quality">Software quality</a></li>

<li><a href="Software_quality_assurance" title="Software quality assurance">Software quality assurance</a></li>

<li><a href="SonarQube" title="SonarQube">SonarQube</a></li></ul></div>

<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .reflist{margin-bottom:0.5em;list-style-type:decimal}@media screen{.mw-parser-output .reflist{font-size:90%}}.mw-parser-output .reflist .references{font-size:100%;margin-bottom:0;list-style-type:inherit}.mw-parser-output .reflist-columns-2{column-width:30em}.mw-parser-output .reflist-columns-3{column-width:25em}.mw-parser-output .reflist-columns{margin-top:0.3em}.mw-parser-output .reflist-columns ol{margin-top:0}.mw-parser-output .reflist-columns li{page-break-inside:avoid;break-inside:avoid-column}.mw-parser-output .reflist-upper-alpha{list-style-type:upper-alpha}.mw-parser-output .reflist-upper-roman{list-style-type:upper-roman}.mw-parser-output .reflist-lower-alpha{list-style-type:lower-alpha}.mw-parser-output .reflist-lower-greek{list-style-type:lower-greek}.mw-parser-output .reflist-lower-roman{list-style-type:lower-roman}

/* end https://en.wikipedia.org/ */

</style><div class="reflist reflist-columns references-column-width" style="column-width: 30em;">

/* start https://en.wikipedia.org/ */

.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("./mw/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("./mw/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("./mw/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("./mw/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}

/* end https://en.wikipedia.org/ */

</style><cite id="CITEREFWichmannCanningClutterbuckWinsbarrow1995" class="citation journal cs1">Wichmann, B. A.; Canning, A. A.; Clutterbuck, D. L.; Winsbarrow, L. A.; Ward, N. J.; Marsh, D. W. R. (Mar 1995). <a rel="nofollow" class="external text" href="https://web.archive.org/web/20110927010304/http://www.ida.liu.se/~TDDC90/papers/industrial95.pdf">"Industrial Perspective on Static Analysis"</a> <span class="cs1-format">(PDF)</span>. <i>Software Engineering Journal</i>. <b>10</b> (2): <span class="nowrap">69–</span>75. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1049%2Fsej.1995.0010">10.1049/sej.1995.0010</a>. Archived from <a rel="nofollow" class="external text" href="http://www.ida.liu.se/~TDDC90/papers/industrial95.pdf">the original</a> <span class="cs1-format">(PDF)</span> on 2011-09-27.</cite></span>

</li>

<li id="cite_note-2"><span class="mw-cite-backlink"><b><a href="#cite_ref-2">^</a></b></span> <span class="reference-text"><cite id="CITEREFEgeleScholteKirdaKruegel2008" class="citation journal cs1">Egele, Manuel; Scholte, Theodoor; Kirda, Engin; Kruegel, Christopher (2008-03-05). <span class="id-lock-subscription" title="Paid subscription required"><a rel="nofollow" class="external text" href="https://doi.org/10.1145/2089125.2089126">"A survey on automated dynamic malware-analysis techniques and tools"</a></span>. <i>ACM Computing Surveys</i>. <b>44</b> (2): 6:1–6:42. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1145%2F2089125.2089126">10.1145/2089125.2089126</a>. <a href="ISSN_(identifier)" class="mw-redirect" title="ISSN (identifier)">ISSN</a> <a rel="nofollow" class="external text" href="https://search.worldcat.org/issn/0360-0300">0360-0300</a>. <a href="S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:1863333">1863333</a>.</cite></span>

</li>

<li id="cite_note-3"><span class="mw-cite-backlink"><b><a href="#cite_ref-3">^</a></b></span> <span class="reference-text"><cite id="CITEREFKhatiwadaTushevMahmoud2018" class="citation journal cs1">Khatiwada, Saket; Tushev, Miroslav; Mahmoud, Anas (2018-01-01). <span class="id-lock-subscription" title="Paid subscription required"><a rel="nofollow" class="external text" href="https://linkinghub.elsevier.com/retrieve/pii/S0950584916302269">"Just enough semantics: An information theoretic approach for IR-based software bug localization"</a></span>. <i>Information and Software Technology</i>. <b>93</b>: <span class="nowrap">45–</span>57. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1016%2Fj.infsof.2017.08.012">10.1016/j.infsof.2017.08.012</a>.</cite></span>

</li>

<li id="cite_note-4"><span class="mw-cite-backlink"><b><a href="#cite_ref-4">^</a></b></span> <span class="reference-text"><a rel="nofollow" class="external text" href="http://web1.see.asso.fr/erts2010/Site/0ANDGY78/Fichier/PAPIERS%20ERTS%202010/ERTS2010_0035_final.pdf">"Software Quality Objectives for Source Code"</a> <a rel="nofollow" class="external text" href="https://web.archive.org/web/20150604203133/http://web1.see.asso.fr/erts2010/Site/0ANDGY78/Fichier/PAPIERS%20ERTS%202010/ERTS2010_0035_final.pdf">Archived</a> 2015-06-04 at the <a href="Wayback_Machine" title="Wayback Machine">Wayback Machine</a> (PDF). <i>Proceedings: Embedded Real Time Software and Systems 2010 Conference</i>, ERTS2010.org, Toulouse, France: Patrick Briand, Martin Brochet, Thierry Cambois, Emmanuel Coutenceau, Olivier Guetta, Daniel Mainberte, Frederic Mondot, Patrick Munier, Loic Noury, Philippe Spozio, Frederic Retailleau.</span>

</li>

<li id="cite_note-5"><span class="mw-cite-backlink"><b><a href="#cite_ref-5">^</a></b></span> <span class="reference-text"><a rel="nofollow" class="external text" href="http://research.microsoft.com/en-us/um/people/livshits/papers/pdf/thesis.pdf"><i>Improving Software Security with Precise Static and Runtime Analysis</i></a> <a rel="nofollow" class="external text" href="https://web.archive.org/web/20110605125310/http://research.microsoft.com/en-us/um/people/livshits/papers/pdf/thesis.pdf">Archived</a> 2011-06-05 at the <a href="Wayback_Machine" title="Wayback Machine">Wayback Machine</a> (PDF), Benjamin Livshits, section 7.3 "Static Techniques for Security". Stanford doctoral thesis, 2006.</span>

</li>

<li id="cite_note-6"><span class="mw-cite-backlink"><b><a href="#cite_ref-6">^</a></b></span> <span class="reference-text"><cite id="CITEREFFDA2010" class="citation web cs1">FDA (2010-09-08). <a rel="nofollow" class="external text" href="https://web.archive.org/web/20100901084658/https://www.fda.gov/MedicalDevices/ProductsandMedicalProcedures/GeneralHospitalDevicesandSupplies/InfusionPumps/ucm202511.htm">"Infusion Pump Software Safety Research at FDA"</a>. Food and Drug Administration. Archived from <a rel="nofollow" class="external text" href="https://www.fda.gov/MedicalDevices/ProductsandMedicalProcedures/GeneralHospitalDevicesandSupplies/InfusionPumps/ucm202511.htm">the original</a> on 2010-09-01<span class="reference-accessdate">. Retrieved <span class="nowrap">2010-09-09</span></span>.</cite></span>

</li>

<li id="cite_note-7"><span class="mw-cite-backlink"><b><a href="#cite_ref-7">^</a></b></span> <span class="reference-text">Computer based safety systems - technical guidance for assessing software aspects of digital computer based protection systems, <cite class="citation web cs1"><a rel="nofollow" class="external text" href="http://webarchive.nationalarchives.gov.uk/20130104193206/http://www.hse.gov.uk/nuclear/operational/tech_asst_guides/tast046.pdf">"Computer based safety systems"</a> <span class="cs1-format">(PDF)</span>. Archived from <a rel="nofollow" class="external text" href="http://www.hse.gov.uk/nuclear/operational/tech_asst_guides/tast046.pdf">the original</a> <span class="cs1-format">(PDF)</span> on January 4, 2013<span class="reference-accessdate">. Retrieved <span class="nowrap">May 15,</span> 2013</span>.</cite></span>

</li>

<li id="cite_note-8"><span class="mw-cite-backlink"><b><a href="#cite_ref-8">^</a></b></span> <span class="reference-text"><a rel="nofollow" class="external text" href="http://www.faa.gov/aircraft/air_cert/design_approvals/air_software/cast/cast_papers/media/cast-9.pdf">Position Paper CAST-9. Considerations for Evaluating Safety Engineering Approaches to Software Assurance</a> <a rel="nofollow" class="external text" href="https://web.archive.org/web/20131006134233/http://www.faa.gov/aircraft/air_cert/design_approvals/air_software/cast/cast_papers/media/cast-9.pdf">Archived</a> 2013-10-06 at the <a href="Wayback_Machine" title="Wayback Machine">Wayback Machine</a> // FAA, Certification Authorities Software Team (CAST), January, 2002: "Verification. A combination of both static and dynamic analyses should be specified by the applicant/developer and applied to the software."</span>

</li>

<cite id="CITEREFVDC_Research2012" class="citation web cs1">VDC Research (2012-02-01). <a rel="nofollow" class="external text" href="http://alm.parasoft.com/embedded-software-vdc-report/">"Automated Defect Prevention for Embedded Software Quality"</a>. VDC Research. <a rel="nofollow" class="external text" href="https://web.archive.org/web/20120411211422/http://alm.parasoft.com/embedded-software-vdc-report/">Archived</a> from the original on 2012-04-11<span class="reference-accessdate">. Retrieved <span class="nowrap">2012-04-10</span></span>.</cite></span>

</li>

<li id="cite_note-10"><span class="mw-cite-backlink"><b><a href="#cite_ref-10">^</a></b></span> <span class="reference-text">Prause, Christian R., René Reiners, and Silviya Dencheva. "Empirical study of tool support in highly distributed research projects." Global Software Engineering (ICGSE), 2010 5th IEEE International Conference on. IEEE, 2010 <a rel="nofollow" class="external free" href="https://ieeexplore.ieee.org/Xplore/login.jsp?url=%2Fielx5%2F5581168%2F5581493%2F05581551.pdf&authDecision=-203">https://ieeexplore.ieee.org/Xplore/login.jsp?url=%2Fielx5%2F5581168%2F5581493%2F05581551.pdf&authDecision=-203</a></span>

</li>

<li id="cite_note-11"><span class="mw-cite-backlink"><b><a href="#cite_ref-11">^</a></b></span> <span class="reference-text">M. Howard and S. Lipner. The Security Development Lifecycle: SDL: A Process for Developing Demonstrably More Secure Software. Microsoft Press, 2006. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-0735622142</bdi></span>

</li>

<li id="cite_note-12"><span class="mw-cite-backlink"><b><a href="#cite_ref-12">^</a></b></span> <span class="reference-text">Achim D. Brucker and Uwe Sodan. <a rel="nofollow" class="external text" href="https://www.brucker.ch/bibliography/download/2014/brucker.ea-sast-expierences-2014.pdf">Deploying Static Application Security Testing on a Large Scale</a> <a rel="nofollow" class="external text" href="https://web.archive.org/web/20141021065105/http://www.brucker.ch/bibliography/download/2014/brucker.ea-sast-expierences-2014.pdf">Archived</a> 2014-10-21 at the <a href="Wayback_Machine" title="Wayback Machine">Wayback Machine</a>. In GI Sicherheit 2014. Lecture Notes in Informatics, 228, pages 91-101, GI, 2014. </span>

</li>

<li id="cite_note-13"><span class="mw-cite-backlink"><b><a href="#cite_ref-13">^</a></b></span> <span class="reference-text"><cite class="citation web cs1"><a rel="nofollow" class="external text" href="http://www.omg.org/CISQ_compliant_IT_Systemsv.4-3.pdf">"OMG Whitepaper | CISQ - Consortium for Information & Software Quality"</a> <span class="cs1-format">(PDF)</span>. <a rel="nofollow" class="external text" href="https://web.archive.org/web/20131228132152/http://www.omg.org/CISQ_compliant_IT_Systemsv.4-3.pdf">Archived</a> <span class="cs1-format">(PDF)</span> from the original on 2013-12-28<span class="reference-accessdate">. Retrieved <span class="nowrap">2013-10-18</span></span>.</cite></span>

</li>

<li id="cite_note-14"><span class="mw-cite-backlink"><b><a href="#cite_ref-14">^</a></b></span> <span class="reference-text"><cite id="CITEREFVijay_D’Silva2008" class="citation web cs1">Vijay D’Silva; et al. (2008). <a rel="nofollow" class="external text" href="http://www.kroening.com/papers/tcad-sw-2008.pdf">"A Survey of Automated Techniques for Formal Software Verification"</a> <span class="cs1-format">(PDF)</span>. Transactions On CAD. <a rel="nofollow" class="external text" href="https://web.archive.org/web/20160304074248/http://www.kroening.com/papers/tcad-sw-2008.pdf">Archived</a> <span class="cs1-format">(PDF)</span> from the original on 2016-03-04<span class="reference-accessdate">. Retrieved <span class="nowrap">2015-05-11</span></span>.</cite></span>

</li>

<li id="cite_note-15"><span class="mw-cite-backlink"><b><a href="#cite_ref-15">^</a></b></span> <span class="reference-text"><cite id="CITEREFJones2010" class="citation web cs1">Jones, Paul (2010-02-09). <a rel="nofollow" class="external text" href="https://web.archive.org/web/20110710185427/http://embeddeddsp.embedded.com/design/opensource/222700533">"A Formal Methods-based verification approach to medical device software analysis"</a>. Embedded Systems Design. Archived from <a rel="nofollow" class="external text" href="https://embeddeddsp.embedded.com/design/opensource/222700533">the original</a> on July 10, 2011<span class="reference-accessdate">. Retrieved <span class="nowrap">2010-09-09</span></span>.</cite></span>

</li>

<li id="cite_note-dewes-16"><span class="mw-cite-backlink">^ <a href="#cite_ref-dewes_16-0"><sup><i><b>a</b></i></sup></a> <a href="#cite_ref-dewes_16-1"><sup><i><b>b</b></i></sup></a></span> <span class="reference-text"><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://www.slideshare.net/japh44/talk-handout-46938511">"Learning from other's mistakes: Data-driven code analysis"</a>. <i>www.slideshare.net</i>. 13 April 2015.</cite></span>

</li>

<li id="cite_note-17"><span class="mw-cite-backlink"><b><a href="#cite_ref-17">^</a></b></span> <span class="reference-text"><cite id="CITEREFSöderbergChurchHöst2021" class="citation book cs1">Söderberg, Emma; Church, Luke; Höst, Martin (2021-06-21). <a rel="nofollow" class="external text" href="https://doi.org/10.1145/3463274.3463808">"Open Data-driven Usability Improvements of Static Code Analysis and its Challenges"</a>. <i>Evaluation and Assessment in Software Engineering</i>. EASE '21. New York, NY, USA: Association for Computing Machinery. pp. <span class="nowrap">272–</span>277. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1145%2F3463274.3463808">10.1145/3463274.3463808</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-1-4503-9053-8</bdi>.</cite></span>

</li>

<li id="cite_note-OhYang2015-18"><span class="mw-cite-backlink"><b><a href="#cite_ref-OhYang2015_18-0">^</a></b></span> <span class="reference-text"><cite id="CITEREFOhYangYi2015" class="citation book cs1">Oh, Hakjoo; Yang, Hongseok; Yi, Kwangkeun (2015). "Learning a strategy for adapting a program analysis via bayesian optimisation". <a rel="nofollow" class="external text" href="https://ora.ox.ac.uk/objects/uuid:f656bcfd-ec1b-477c-9185-ff2c7490a207"><i>Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications - OOPSLA 2015</i></a>. pp. <span class="nowrap">572–</span>588. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1145%2F2814270.2814309">10.1145/2814270.2814309</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>9781450336895</bdi>. <a href="S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:13940725">13940725</a>.</cite></span>

</li>

<li id="cite_note-19"><span class="mw-cite-backlink"><b><a href="#cite_ref-19">^</a></b></span> <span class="reference-text"><cite id="CITEREFLogozzoBall2012" class="citation journal cs1">Logozzo, Francesco; Ball, Thomas (2012-11-15). <span class="id-lock-subscription" title="Paid subscription required"><a rel="nofollow" class="external text" href="https://dx.doi.org/10.1145/2398857.2384626">"Modular and verified automatic program repair"</a></span>. <i>ACM SIGPLAN Notices</i>. <b>47</b> (10): <span class="nowrap">133–</span>146. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1145%2F2398857.2384626">10.1145/2398857.2384626</a>. <a href="ISSN_(identifier)" class="mw-redirect" title="ISSN (identifier)">ISSN</a> <a rel="nofollow" class="external text" href="https://search.worldcat.org/issn/0362-1340">0362-1340</a>.</cite></span>

</li>

</ol></div>

<div class="mw-heading mw-heading2"><h2 id="Further_reading">Further reading</h2></div>

<ul><li><cite id="CITEREFAyewahHovemeyerMorgenthalerPenix2008" class="citation journal cs1">Ayewah, Nathaniel; Hovemeyer, David; Morgenthaler, J. David; Penix, John; Pugh, William (2008). "Using Static Analysis to Find Bugs". <i>IEEE Software</i>. <b>25</b> (5): <span class="nowrap">22–</span>29. <a href="CiteSeerX_(identifier)" class="mw-redirect" title="CiteSeerX (identifier)">CiteSeerX</a> <span class="id-lock-free" title="Freely accessible"><a rel="nofollow" class="external text" href="https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.187.8985">10.1.1.187.8985</a></span>. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1109%2FMS.2008.130">10.1109/MS.2008.130</a>. <a href="S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:20646690">20646690</a>.</cite></li>

<li><cite id="CITEREFBrian_Chess,_Jacob_West_(Fortify_Software)2007" class="citation book cs1">Brian Chess, Jacob West (Fortify Software) (2007). <i>Secure Programming with Static Analysis</i>. Addison-Wesley. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-0-321-42477-8</bdi>.</cite></li>

<li><cite id="CITEREFFlemming_NielsonHanne_R._NielsonChris_Hankin2004" class="citation book cs1">Flemming Nielson; Hanne R. Nielson; Chris Hankin (2004-12-10). <i>Principles of Program Analysis</i> (1999 (corrected 2004) ed.). Springer. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-3-540-65410-0</bdi>.</cite></li>

<li><a rel="nofollow" class="external text" href="http://santos.cis.ksu.edu/schmidt/Escuela03/home.html">"Abstract interpretation and static analysis,"</a> International Winter School on Semantics and Applications 2003, by <a rel="nofollow" class="external text" href="http://people.cis.ksu.edu/~schmidt/">David A. Schmidt</a></li></ul>

/* start https://en.wikipedia.org/ */

.mw-parser-output .navbox{box-sizing:border-box;border:1px solid #a2a9b1;width:100%;clear:both;font-size:88%;text-align:center;padding:1px;margin:1em auto 0}.mw-parser-output .navbox .navbox{margin-top:0}.mw-parser-output .navbox+.navbox,.mw-parser-output .navbox+.navbox-styles+.navbox{margin-top:-1px}.mw-parser-output .navbox-inner,.mw-parser-output .navbox-subgroup{width:100%}.mw-parser-output .navbox-group,.mw-parser-output .navbox-title,.mw-parser-output .navbox-abovebelow{padding:0.25em 1em;line-height:1.5em;text-align:center}.mw-parser-output .navbox-group{white-space:nowrap;text-align:right}.mw-parser-output .navbox,.mw-parser-output .navbox-subgroup{background-color:#fdfdfd}.mw-parser-output .navbox-list{line-height:1.5em;border-color:#fdfdfd}.mw-parser-output .navbox-list-with-group{text-align:left;border-left-width:2px;border-left-style:solid}.mw-parser-output tr+tr>.navbox-abovebelow,.mw-parser-output tr+tr>.navbox-group,.mw-parser-output tr+tr>.navbox-image,.mw-parser-output tr+tr>.navbox-list{border-top:2px solid #fdfdfd}.mw-parser-output .navbox-title{background-color:#ccf}.mw-parser-output .navbox-abovebelow,.mw-parser-output .navbox-group,.mw-parser-output .navbox-subgroup .navbox-title{background-color:#ddf}.mw-parser-output .navbox-subgroup .navbox-group,.mw-parser-output .navbox-subgroup .navbox-abovebelow{background-color:#e6e6ff}.mw-parser-output .navbox-even{background-color:#f7f7f7}.mw-parser-output .navbox-odd{background-color:transparent}.mw-parser-output .navbox .hlist td dl,.mw-parser-output .navbox .hlist td ol,.mw-parser-output .navbox .hlist td ul,.mw-parser-output .navbox td.hlist dl,.mw-parser-output .navbox td.hlist ol,.mw-parser-output .navbox td.hlist ul{padding:0.125em 0}.mw-parser-output .navbox .navbar{display:block;font-size:100%}.mw-parser-output .navbox-title .navbar{float:left;text-align:left;margin-right:0.5em}body.skin--responsive .mw-parser-output .navbox-image img{max-width:none!important}@media print{body.ns-0 .mw-parser-output .navbox{display:none!important}}

/* end https://en.wikipedia.org/ */

</style></div><div role="navigation" class="navbox" aria-labelledby="Program_analysis496" style="padding:3px"><table class="nowraplinks hlist mw-collapsible expanded navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="3"><div id="Program_analysis496" style="font-size:114%;margin:0 4em"><a href="Program_analysis" title="Program analysis">Program analysis</a></div></th></tr><tr><th scope="row" class="navbox-group" style="width:1%;background:#e5e5ff;">Key<br>concepts</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Control-flow_graph" title="Control-flow graph">Control-flow graph</a></li>

<li><a href="Correctness_(computer_science)" title="Correctness (computer science)">Correctness</a></li>

<li><a href="Hyperproperty" title="Hyperproperty">Hyperproperties</a></li>

<li><a href="Invariant_(computer_science)" class="mw-redirect" title="Invariant (computer science)">Invariants</a></li>

<li><a href="Path_explosion" title="Path explosion">Path explosion</a></li>

<li><a href="Polyvariance" title="Polyvariance">Polyvariance</a></li>

<li><a href="Rice's_theorem" title="Rice's theorem">Rice's theorem</a></li>

<li><a href="Runtime_verification" title="Runtime verification">Runtime verification</a></li>

<li><a href="Safety_and_liveness_properties" title="Safety and liveness properties">Safety and liveness</a></li>

<li><a href="Undefined_behavior" title="Undefined behavior">Undefined behavior</a></li></ul>

</div></td><td class="noviewer navbox-image" rowspan="4" style="width:1px;padding:0 0 0 2px"><div><span typeof="mw:File"></span></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%;background:#e5e5ff;"><a href="Semantics_(computer_science)" title="Semantics (computer science)">Semantics</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%">Types</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Axiomatic_semantics" title="Axiomatic semantics">Axiomatic</a></li>

<li><a href="Denotational_semantics" title="Denotational semantics">Denotational</a>

<ul><li><a href="Categorical_logic" title="Categorical logic">Categorical semantics</a></li></ul></li>

<li><a href="Operational_semantics" title="Operational semantics">Operational</a>

<li><a href="Small_Step_Semantics" class="mw-redirect" title="Small Step Semantics">Small-step</a></li></ul></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Model_of_computation" title="Model of computation">Models</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Lambda_calculus" title="Lambda calculus">Lambda calculus</a></li>

<li><a href="Petri_net" title="Petri net">Petri net</a></li>

<li><a href="Process_calculus" title="Process calculus">Process calculus</a></li>

<li><a href="Abstract_rewriting_system" title="Abstract rewriting system">Rewriting system</a></li>

<li><a href="Finite-state_machine" title="Finite-state machine">State machine</a></li>

<li><a href="Turing_machine" title="Turing machine">Turing machine</a></li></ul>

</div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%;background:#e5e5ff;">Analyses</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%"></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Abstract_interpretation" title="Abstract interpretation">Abstract interpretation</a></li>

<li><a href="Alias_analysis" title="Alias analysis">Alias</a></li>

<li><a href="Control-flow_analysis" title="Control-flow analysis">Control flow</a>

<li><a href="Dependence_analysis" title="Dependence analysis">Dependence</a></li>

<li><a href="Effect_system" title="Effect system">Effect system</a></li>

<li><a href="Escape_analysis" title="Escape analysis">Escape</a></li>

<li><a href="Model_checking" title="Model checking">Model checking</a></li>

<li><a href="Pointer_analysis" title="Pointer analysis">Pointer</a></li>

<li><a href="Shape_analysis_(program_analysis)" title="Shape analysis (program analysis)">Shape</a></li>

<li><a href="Symbolic_execution" title="Symbolic execution">Symbolic execution</a></li>

<li><a href="Termination_analysis" title="Termination analysis">Termination</a></li>

<li><a href="Type_system" title="Type system">Type systems</a></li>

<li><a href="Typestate_analysis" title="Typestate analysis">Typestate</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Dynamic_program_analysis" title="Dynamic program analysis">Dynamic</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li>Taint tracking</li></ul></li>

<li><a href="Concolic_testing" title="Concolic testing">Concolic testing</a></li>

<li><a href="Fuzzing" title="Fuzzing">Fuzzing</a></li>

<li>Invariant inference</li>

<li><a href="Program_slicing" title="Program slicing">Program slicing</a></li>

<li><a href="Software_testing" title="Software testing">Testing</a></li></ul>

</div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%;background:#e5e5ff;"><a href="Formal_methods" title="Formal methods">Formal<br>methods</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%">Concepts</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Curry%E2%80%93Howard_correspondence" title="Curry–Howard correspondence">Curry–Howard correspondence</a></li>

<li><a href="Loop_invariant" title="Loop invariant">Loop invariant</a></li>

<li><a href="Refinement_(computing)" title="Refinement (computing)">Refinement</a></li>

<li><a href="Side_effect_(computer_science)" title="Side effect (computer science)">Side effect</a></li>

<li><a href="Soundness" title="Soundness">Soundness</a> and <a href="Completeness_(logic)" title="Completeness (logic)">completeness</a></li>

<li><a href="Formal_specification" title="Formal specification">Specification</a>

<ul><li><a href="Specification_language" title="Specification language">Languages</a></li></ul></li>

<li><a href="Formal_verification" title="Formal verification">Verification</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Logics</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Hoare_logic" title="Hoare logic">Hoare</a></li>

<li>Incorrectness</li>

<li><a href="Linear_logic" title="Linear logic">Linear</a></li>

<li><a href="Separation_logic" title="Separation logic">Separation</a></li>

<li><a href="Temporal_logic" title="Temporal logic">Temporal</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Data_structure" title="Data structure">Data structures</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<li><a href="E-graph" title="E-graph">E-graph</a></li>

<li><a href="Hash_consing" title="Hash consing">Hashcons</a></li>

<li><a href="Disjoint-set_data_structure" title="Disjoint-set data structure">Union-find</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Tools</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Constraint_programming" title="Constraint programming">Constraint solvers</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Formal_methods#Lightweight_formal_methods" title="Formal methods">Lightweight</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Alloy_(specification_language)" title="Alloy (specification language)">Alloy</a></li>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Proof_assistant" title="Proof assistant">Proof assistants</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<li><a href="HOL_Light" title="HOL Light">HOL Light</a></li>

<li><a href="Idris_(programming_language)" title="Idris (programming language)">Idris</a></li>

<li><a href="Isabelle_(proof_assistant)" title="Isabelle (proof assistant)">Isabelle</a>

<ul><li><a href="Isabelle/HOL" class="mw-redirect" title="Isabelle/HOL">Isabelle/HOL</a></li></ul></li>

<li><a href="Mizar_system" title="Mizar system">Mizar</a></li>

<li><a href="Nuprl" title="Nuprl">NuPRL</a></li>

<li><a href="Twelf" title="Twelf">Twelf</a></li></ul>

</div></td></tr></tbody></table><div></div></td></tr></tbody></table><div></div></td></tr><tr><td class="navbox-abovebelow" colspan="3" style="font-weight:bold;"><div>

<ul><li><span class="noviewer" typeof="mw:File"><span title="Category"></span></span> Category</li>

<li><span class="noviewer" typeof="mw:File"><span title="List-Class article"></span></span> Outline</li>

<li><span class="noviewer" typeof="mw:File"><span title="List-Class article"></span></span> Glossary</li></ul>

</div></td></tr></tbody></table></div></div><div><div class="zim-footer">

This article is issued from <a class="external text" title="Last edited on 2025-05-29" href="https://en.wikipedia.org/wiki/?title=Static_program_analysis&oldid=1292971924">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.

</div>

</div></div>

</div>

</main>

</div>

</body></html>